The invention relates to software design and validation.
An important aspect of software development involves validating that an implementation of a design will function correctly and have desired operating properties. Over time, software systems have become increasingly complex and validation of these systems has become increasingly difficult. This is particularly true of distributed systems that are formed from multiple interacting and asynchronously operating components. Distributed systems include not only physically distributed architectures in which components execute on physically separated computers coupled by communication paths, for example, over data networks, but also include architectures in which multiple components execute on a single computer and are controlled as distinct tasks (e.g., processes or threads). In order to validate such software systems, ad hoc approaches to testing cannot in general be relied on due to the complexity of the overall system.
Formal specifications for abstracted designs of software systems have been used to validate properties of the abstracted designs. One approach to specifying such designs uses the formalism of Input/Output (I/O) Automata, as described in Chapter 8 of the textbook, Distributed Algorithms, by Nancy Lynch (Morgan Kaufmann Publishers, 1996, ISBN 1-55860-348-4), which is incorporated herein by reference. An I/O automaton is a labeled transition system model (i.e., a state machine with labeled state transitions) for one or more components of a system, and can be used to model components of an asynchronous concurrent system.
One method of validating properties of a system design, in particular of system designs specified using I/O automata, uses a theorem proving approach. In such an approach, properties of the system design that are to be validated are expressed as logical assertions (predicates), and underlying statements about the system design are expressed as logical axioms. The axioms generally relate to the detailed operation of the system, while the assertions relate to the overall aspects of its desired behavior. A user then verifies by hand that the properties are necessarily true given the axioms, or may possibly use a user-assisted program, such as a theorem proving program, to aid in this verification.
Other methods for validating system properties can also be used. One approach, known as "model checking," is based on exhaustive checking of all states in an instance of a system design in which the size of the system (i.e., the number of states) is restricted. Another approach is based on simulation of the operation of the system, in which a typically more complex (e.g., larger number of states) instance of the system is checked by examining a sample sequence of states or of transition labels ("actions") resulting from execution of the system.